perm filename WISEMA.PRF[S78,JMC] blob
sn#363918 filedate 1978-06-24 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002
C00026 ENDMK
C⊗;
*****ASSUME A(RW,w,W3,2);
1 A(RW,w,W3,2) (1)
*****ASSUME color(W3,w)=B;
2 color(W3,w)=B (2)
*****ASSUME A(w,w1,W2,1);
3 A(w,w1,W2,1) (3)
*****ASSUME color(W2,w1)=B;
4 color(W2,w1)=B (4)
*****ASSUME A(w1,w2,W1,0);
5 A(w1,w2,W1,0) (5)
*****∀E elwek21 w;
6 A(RW,w,W123,2)≡(A(RW,w,W123,1)∧∀p.(∀w1.(A(w,w1,p,1)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,1)⊃color(p,w1)=colo%
r(p,RW))))
*****∀E elwek11 w;
7 A(RW,w,W123,1)≡(A(RW,w,W123,0)∧∀p.(∀w1.(A(w,w1,p,0)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=colo%
r(p,RW))))
*****∀E w123 RW,w,2;
8 (A(RW,w,W1,2)∨(A(RW,w,W2,2)∨A(RW,w,W3,2)))⊃A(RW,w,W123,2)
*****TAUT A(RW,w,W123,0) 1:8;
9 A(RW,w,W123,0) (1 2 3 4 5)
*****∀E elwek13 w,w1;
10 A(w,w1,W2,1)≡(A(w,w1,W2,0)∧A(w,w1,W123,1))
*****∀E w123 w,w1,0;
11 (A(w,w1,W1,0)∨(A(w,w1,W2,0)∨A(w,w1,W3,0)))⊃A(w,w1,W123,0)
*****TAUT A(w,w1,W123,0) 3,10:11;
12 A(w,w1,W123,0) (3)
*****∀E w123 w1,w2,0;
13 (A(w1,w2,W1,0)∨(A(w1,w2,W2,0)∨A(w1,w2,W3,0)))⊃A(w1,w2,W123,0)
*****∀E transitive w,w1,w2,W123,0;
14 (A(w,w1,W123,0)∧A(w1,w2,W123,0))⊃A(w,w2,W123,0)
*****∀E transitive RW,w,w2,W123,0;
15 (A(RW,w,W123,0)∧A(w,w2,W123,0))⊃A(RW,w2,W123,0)
*****TAUT A(RW,w2,W123,0) 1:15;
16 A(RW,w2,W123,0) (1 2 3 4 5)
*****∀E king w2;
17 A(RW,w2,W123,0)⊃(color(W1,w2)=W∨(color(W2,w2)=W∨color(W3,w2)=W))
*****∀E initial2 w1,w2;
18 (A(RW,w1,W123,0)∧A(w1,w2,W1,0))⊃(color(W2,w2)=color(W2,w1)∧color(W3,w2)=color(W3,w1))
*****∀E transitive RW,w,w1,W123,0;
19 (A(RW,w,W123,0)∧A(w,w1,W123,0))⊃A(RW,w1,W123,0)
*****TAUTEQ color(W2,w2)=B color1,1:19;
20 color(W2,w2)=B (1 2 3 4 5)
*****∀E initial3 w,w1;
21 (A(RW,w,W123,0)∧A(w,w1,W2,0))⊃(color(W1,w1)=color(W1,w)∧color(W3,w1)=color(W3,w))
*****TAUTEQ color(W3,w1)=B color1,1:21;
22 color(W3,w1)=B (1 2 3 4 5)
*****TAUTEQ color(W3,w2)=B color1,1:22;
23 color(W3,w2)=B (1 2 3 4 5)
*****TAUTEQ color(W1,w2)=W color1,1:23;
24 color(W1,w2)=W (1 2 3 4 5)
*****∀E initial4 RW,w;
25 (A(RW,RW,W123,0)∧A(RW,w,W3,0))⊃(color(W1,w)=color(W1,RW)∧color(W2,w)=color(W2,RW))
*****∀E reflex RW,W123,0;
26 A(RW,RW,W123,0)
*****∀E elwek24 RW,w;
27 A(RW,w,W3,2)≡(A(RW,w,W3,1)∧A(RW,w,W123,1))
*****∀E elwek14 RW,w;
28 A(RW,w,W3,1)≡(A(RW,w,W3,0)∧A(RW,w,W123,1))
*****TAUTEQ color(W1,w)=W rw,1:28;
29 color(W1,w)=W (1 2 3 4 5)
*****∀E initial3 w,w1;
30 (A(RW,w,W123,0)∧A(w,w1,W2,0))⊃(color(W1,w1)=color(W1,w)∧color(W3,w1)=color(W3,w))
*****∀E elwek13 w,w1;
31 A(w,w1,W2,1)≡(A(w,w1,W2,0)∧A(w,w1,W123,1))
*****TAUTEQ color(W1,w2)=color(W1,w1) 1:31;
32 color(W1,w2)=color(W1,w1) (1 2 3 4 5)
*****⊃I 5⊃↑;
33 A(w1,w2,W1,0)⊃color(W1,w2)=color(W1,w1) (1 2 3 4)
*****∀I ↑ w2;
34 ∀w2.(A(w1,w2,W1,0)⊃color(W1,w2)=color(W1,w1)) (1 2 3 4)
*****∀E elwek11 w1;
35 A(RW,w1,W123,1)≡(A(RW,w1,W123,0)∧∀p.(∀w.(A(w1,w,p,0)⊃color(p,w)=color(p,w1))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=co%
lor(p,RW))))
*****∀E transitive RW,w,w1,W123,1;
36 (A(RW,w,W123,1)∧A(w,w1,W123,1))⊃A(RW,w1,W123,1)
*****TAUT ∀p.(∀w.(A(w1,w,p,0)⊃color(p,w)=color(p,w1))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW))) 1,3,6:8,10:12,%
35:36;
37 ∀p.(∀w.(A(w1,w,p,0)⊃color(p,w)=color(p,w1))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW))) (1 3)
*****∀E ↑ W1;
38 ∀w.(A(w1,w,W1,0)⊃color(W1,w)=color(W1,w1))≡∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) (1 3)
*****UNIFY ∀w.(A(w1,w,W1,0)⊃color(W1,w)=color(W1,w1)) 34;
39 ∀w.(A(w1,w,W1,0)⊃color(W1,w)=color(W1,w1)) (1 2 3 4)
*****TAUT ∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) 38:39;
40 ∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) (1 2 3 4)
*****∀E initial1 B,RW;
41 A(RW,RW,W123,0)⊃(((B=W∨(color(W2,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B))∧(((B=W∨(color(W1,%
RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B))∧((B=W∨(color(W1,RW)=W∨color(W2,RW)=W))⊃∃w1.(A(RW,w1,W%
3,0)∧color(W3,w1)=B))))
*****TAUTEQ ∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B) rw,26,41;
42 ∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B)
*****∃E ↑ w3;
43 A(RW,w3,W1,0)∧color(W1,w3)=B (43)
*****∀E 40 w3;
44 A(RW,w3,W1,0)⊃color(W1,w3)=color(W1,RW) (1 2 3 4)
*****TAUTEQ FALSE color1,rw,43:44;
45 FALSE (1 2 3 4)
*****¬I ↑,color(W2,w1)=B;
46 ¬(color(W2,w1)=B) (1 2 3)
*****∀E color2 color(W2,w1);
47 color(W2,w1)=W∨color(W2,w1)=B
*****TAUTEQ color(W2,w1)=W 46:47;
48 color(W2,w1)=W (1 2 3)
*****∀E initial4 RW,w;
49 (A(RW,RW,W123,0)∧A(RW,w,W3,0))⊃(color(W1,w)=color(W1,RW)∧color(W2,w)=color(W2,RW))
*****TAUTEQ color(W2,w1)=color(W2,w) rw,1,26:28,48:49;
50 color(W2,w1)=color(W2,w) (1 2 3)
*****⊃I 3⊃↑;
51 A(w,w1,W2,1)⊃color(W2,w1)=color(W2,w) (1 2)
*****∀I ↑ w1;
52 ∀w1.(A(w,w1,W2,1)⊃color(W2,w1)=color(W2,w)) (1 2)
*****TAUT ∀p.(∀w1.(A(w,w1,p,1)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,1)⊃color(p,w1)=color(p,RW))) 1,6,8;
53 ∀p.(∀w1.(A(w,w1,p,1)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,1)⊃color(p,w1)=color(p,RW))) (1)
*****∀E ↑ W2;
54 ∀w1.(A(w,w1,W2,1)⊃color(W2,w1)=color(W2,w))≡∀w1.(A(RW,w1,W2,1)⊃color(W2,w1)=color(W2,RW)) (1)
*****TAUT ∀w1.(A(RW,w1,W2,1)⊃color(W2,w1)=color(W2,RW)) 52,54;
55 ∀w1.(A(RW,w1,W2,1)⊃color(W2,w1)=color(W2,RW)) (1 2)
*****∀E initial1 B,RW;
56 A(RW,RW,W123,0)⊃(((B=W∨(color(W2,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B))∧(((B=W∨(color(W1,%
RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B))∧((B=W∨(color(W1,RW)=W∨color(W2,RW)=W))⊃∃w1.(A(RW,w1,W%
3,0)∧color(W3,w1)=B))))
*****TAUT ((B=W∨(color(W2,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B))∧(((B=W∨(color(W1,RW)=W∨colo%
r(W3,RW)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B))∧((B=W∨(color(W1,RW)=W∨color(W2,RW)=W))⊃∃w1.(A(RW,w1,W3,0)∧color%
(W3,w1)=B))) 26,56;
57 ((B=W∨(color(W2,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B))∧(((B=W∨(color(W1,RW)=W∨color(W3,RW%
)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B))∧((B=W∨(color(W1,RW)=W∨color(W2,RW)=W))⊃∃w1.(A(RW,w1,W3,0)∧color(W3,w1)%
=B)))
*****TAUT ((B=W∨(color(W1,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B))∧((B=W∨(color(W1,RW)=W∨color%
(W2,RW)=W))⊃∃w1.(A(RW,w1,W3,0)∧color(W3,w1)=B)) 57;
58 ((B=W∨(color(W1,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B))∧((B=W∨(color(W1,RW)=W∨color(W2,RW)%
=W))⊃∃w1.(A(RW,w1,W3,0)∧color(W3,w1)=B))
*****TAUT (B=W∨(color(W1,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B) 58;
59 (B=W∨(color(W1,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B)
*****TAUT ∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B) rw,59;
60 ∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B)
*****∃E ↑ w1;
61 A(RW,w1,W2,0)∧color(W2,w1)=B (61)
*****∀E foolscap w3;
62 color(W123,w3)=W
*****∀E foolscap w1;
63 color(W123,w1)=W
*****∀E foolscap RW;
64 color(W123,RW)=W
*****TAUTEQ A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1) 62:63;
65 A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1)
*****∀I ↑ w3;
66 ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1))
*****TAUTEQ A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW) 62,64;
67 A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW)
*****∀I ↑ w3;
68 ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW))
*****TAUT ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1))≡∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW)%
) 66,68;
69 ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1))≡∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,RW))
*****ASSUME p=W123;
70 p=W123 (70)
*****SUBST ↑ IN ↑↑;
71 ∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,RW)) (70)
*****⊃I ↑↑⊃↑;
72 p=W123⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,RW)))
*****∀E initial1 B,RW;
73 A(RW,RW,W123,0)⊃(((B=W∨(color(W2,RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B))∧(((B=W∨(color(W1,%
RW)=W∨color(W3,RW)=W))⊃∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B))∧((B=W∨(color(W1,RW)=W∨color(W2,RW)=W))⊃∃w1.(A(RW,w1,W%
3,0)∧color(W3,w1)=B))))
*****TAUTEQ ∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B) rw,26,73;
74 ∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B)
*****∃E ↑ w1;
75 A(RW,w1,W1,0)∧color(W1,w1)=B (75)
*****TAUTEQ ¬(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) rw,color1,75;
76 ¬(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) (75)
*****∃I ↑ w1 ;
77 ∃w1.¬(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW))
*****UNIFY ¬∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) ↑;
78 ¬∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW))
*****TAUTEQ ∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B) rw,color1,26,73;
79 ∃w1.(A(RW,w1,W2,0)∧color(W2,w1)=B)
*****∃E ↑ w1;
80 A(RW,w1,W2,0)∧color(W2,w1)=B (80)
*****TAUTEQ ¬(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW)) rw,color1,80;
81 ¬(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW)) (80)
*****∃I ↑ w1 ;
82 ∃w1.¬(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW))
*****UNIFY ¬∀w1.(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW)) ↑;
83 ¬∀w1.(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW))
*****TAUTEQ ∃w1.(A(RW,w1,W3,0)∧color(W3,w1)=B) rw,color1,26,73;
84 ∃w1.(A(RW,w1,W3,0)∧color(W3,w1)=B)
*****∃E ↑ w1;
85 A(RW,w1,W3,0)∧color(W3,w1)=B (85)
*****TAUTEQ ¬(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW)) rw,color1,85;
86 ¬(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW)) (85)
*****∃I ↑ w1 ;
87 ∃w1.¬(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW))
*****UNIFY ¬∀w1.(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW)) ↑;
88 ¬∀w1.(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW))
*****∀E w123 RW,w1,0;
89 (A(RW,w1,W1,0)∨(A(RW,w1,W2,0)∨A(RW,w1,W3,0)))⊃A(RW,w1,W123,0)
*****TAUT A(RW,w1,W123,0) 61,89;
90 A(RW,w1,W123,0) (61)
*****∀E initial3 RW,w1;
91 (A(RW,RW,W123,0)∧A(RW,w1,W2,0))⊃(color(W1,w1)=color(W1,RW)∧color(W3,w1)=color(W3,RW))
*****TAUTEQ color(W1,w1)=W∧color(W3,w1)=W rw,26,61,91;
92 color(W1,w1)=W∧color(W3,w1)=W (61)
*****∀E initial1 B,w1;
93 A(RW,w1,W123,0)⊃(((B=W∨(color(W2,w1)=W∨color(W3,w1)=W))⊃∃w.(A(w1,w,W1,0)∧color(W1,w)=B))∧(((B=W∨(color(W1,w1)%
=W∨color(W3,w1)=W))⊃∃w.(A(w1,w,W2,0)∧color(W2,w)=B))∧((B=W∨(color(W1,w1)=W∨color(W2,w1)=W))⊃∃w.(A(w1,w,W3,0)∧col%
or(W3,w)=B))))
*****TAUTEQ ∃w.(A(w1,w,W1,0)∧color(W1,w)=B) 90,92:93;
94 ∃w.(A(w1,w,W1,0)∧color(W1,w)=B) (61)
*****∃E ↑ w3;
95 A(w1,w3,W1,0)∧color(W1,w3)=B (95)
*****TAUTEQ ¬(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1)) color1,92,95;
96 ¬(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1)) (61 95)
*****∃I ↑ w3 ;
97 ∃w3.¬(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1)) (61)
*****UNIFY ¬∀w3.(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1)) ↑;
98 ¬∀w3.(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1)) (61)
*****TAUT ∀w3.(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1))≡∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) 78,98;
99 ∀w3.(A(w1,w3,W1,0)⊃color(W1,w3)=color(W1,w1))≡∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) (61)
*****ASSUME p=W1;
100 p=W1 (100)
*****SUBST ↑ IN ↑↑;
101 ∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW)) (61 100)
*****⊃I ↑↑⊃↑;
102 p=W1⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW))) (61)
*****TAUTEQ A(RW,w3,W123,0)⊃color(W123,w3)=color(W123,RW) 62,64;
103 A(RW,w3,W123,0)⊃color(W123,w3)=color(W123,RW)
*****∀I ↑ w3;
104 ∀w3.(A(RW,w3,W123,0)⊃color(W123,w3)=color(W123,RW))
*****TAUT ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1))≡∀w3.(A(RW,w3,W123,0)⊃color(W123,w3)=color(W123,RW)%
) 66,104;
105 ∀w3.(A(w1,w3,W123,0)⊃color(W123,w3)=color(W123,w1))≡∀w3.(A(RW,w3,W123,0)⊃color(W123,w3)=color(W123,RW))
*****ASSUME p=W123;
106 p=W123 (106)
*****SUBST ↑ IN ↑↑;
107 ∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW)) (106)
*****⊃I ↑↑⊃↑;
108 p=W123⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW)))
*****TAUTEQ p=W1⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW))) 102;
109 p=W1⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW))) (61)
*****TAUTEQ ∃w.(A(w1,w,W3,0)∧color(W3,w)=B) 90,92:93;
110 ∃w.(A(w1,w,W3,0)∧color(W3,w)=B) (61)
*****∃E ↑ w3;
111 A(w1,w3,W3,0)∧color(W3,w3)=B (111)
*****TAUTEQ ¬(A(w1,w3,W3,0)⊃color(W3,w3)=color(W3,w1)) color1,92,111;
112 ¬(A(w1,w3,W3,0)⊃color(W3,w3)=color(W3,w1)) (61 111)
*****∃I ↑ w3 ;
113 ∃w3.¬(A(w1,w3,W3,0)⊃color(W3,w3)=color(W3,w1)) (61)
*****UNIFY ¬∀w3.(A(w1,w3,W3,0)⊃color(W3,w3)=color(W3,w1)) ↑;
114 ¬∀w3.(A(w1,w3,W3,0)⊃color(W3,w3)=color(W3,w1)) (61)
*****TAUT ∀w3.(A(w1,w3,W3,0)⊃color(W3,w3)=color(W3,w1))≡∀w1.(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW)) 88,114;
115 ∀w3.(A(w1,w3,W3,0)⊃color(W3,w3)=color(W3,w1))≡∀w1.(A(RW,w1,W3,0)⊃color(W3,w1)=color(W3,RW)) (61)
*****ASSUME p=W3;
116 p=W3 (116)
*****SUBST ↑ IN ↑↑;
117 ∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW)) (61 116)
*****⊃I ↑↑⊃↑;
118 p=W3⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW))) (61)
*****TAUTEQ p=W3⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW))) 118;
119 p=W3⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW))) (61)
*****∀E initial1 W,w1;
120 A(RW,w1,W123,0)⊃(((W=W∨(color(W2,w1)=W∨color(W3,w1)=W))⊃∃w.(A(w1,w,W1,0)∧color(W1,w)=W))∧(((W=W∨(color(W1,w1%
)=W∨color(W3,w1)=W))⊃∃w.(A(w1,w,W2,0)∧color(W2,w)=W))∧((W=W∨(color(W1,w1)=W∨color(W2,w1)=W))⊃∃w.(A(w1,w,W3,0)∧co%
lor(W3,w)=W))))
*****TAUTEQ ∃w.(A(w1,w,W2,0)∧color(W2,w)=W) 90,120;
121 ∃w.(A(w1,w,W2,0)∧color(W2,w)=W) (61)
*****∃E ↑ w3;
122 A(w1,w3,W2,0)∧color(W2,w3)=W (122)
*****TAUTEQ ¬(A(w1,w3,W2,0)⊃color(W2,w3)=color(W2,w1)) color1,61,122;
123 ¬(A(w1,w3,W2,0)⊃color(W2,w3)=color(W2,w1)) (61 122)
*****∃I ↑ w3 ;
124 ∃w3.¬(A(w1,w3,W2,0)⊃color(W2,w3)=color(W2,w1)) (61)
*****UNIFY ¬∀w3.(A(w1,w3,W2,0)⊃color(W2,w3)=color(W2,w1)) ↑;
125 ¬∀w3.(A(w1,w3,W2,0)⊃color(W2,w3)=color(W2,w1)) (61)
*****TAUT ∀w3.(A(w1,w3,W2,0)⊃color(W2,w3)=color(W2,w1))≡∀w1.(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW)) 83,125;
126 ∀w3.(A(w1,w3,W2,0)⊃color(W2,w3)=color(W2,w1))≡∀w1.(A(RW,w1,W2,0)⊃color(W2,w1)=color(W2,RW)) (61)
*****ASSUME p=W2;
127 p=W2 (127)
*****SUBST ↑ IN ↑↑;
128 ∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW)) (61 127)
*****⊃I ↑↑⊃↑;
129 p=W2⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW))) (61)
*****TAUTEQ p=W2⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW))) 129;
130 p=W2⊃(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW))) (61)
*****∀E who p;
131 p=W1∨(p=W2∨(p=W3∨p=W123))
*****TAUT ∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW)) 108:109,119,130:%
131;
132 ∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW)) (61)
*****∀I ↑ p;
133 ∀p.(∀w3.(A(w1,w3,p,0)⊃color(p,w3)=color(p,w1))≡∀w3.(A(RW,w3,p,0)⊃color(p,w3)=color(p,RW))) (61)